YES 0.382 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/Queue.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



↳ HASKELL
  ↳ BR

mainModule Queue
  ((listToQueue :: [a]  ->  Queue a) :: [a]  ->  Queue a)

module Queue where
  import qualified Prelude
  data Queue a = Q [a] [a] [a] 
  listToQueue :: [a]  ->  Queue a
listToQueue xs = Q xs [] xs



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR

mainModule Queue
  ((listToQueue :: [a]  ->  Queue a) :: [a]  ->  Queue a)

module Queue where
  import qualified Prelude
  data Queue a = Q [a] [a] [a] 
  listToQueue :: [a]  ->  Queue a
listToQueue xs = Q xs [] xs



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow

mainModule Queue
  (listToQueue :: [a]  ->  Queue a)

module Queue where
  import qualified Prelude
  data Queue a = Q [a] [a] [a] 
  listToQueue :: [a]  ->  Queue a
listToQueue xs = Q xs [] xs



Haskell To QDPs